This repository contains the source code of the fully verified EiffelBase2 library. All classes can be verified using a web interface following the links below.
| Class | Description | . |
|---|---|---|
| CONTAINER | Containers for a finite number of values. | verify |
| INPUT_STREAM | Streams that provide values one by one. | verify |
| OUTPUT_STREAM | Streams where values can be output one by one. | verify |
| ITERATOR | Iterators to read from a container in linear order. | verify |
| SEQUENCE | Containers where values are associated with integer indexes from a continuous interval. | verify |
| SEQUENCE_ITERATOR | Itreators to read from sequences. | verify |
| MUTABLE_SEQUENCE | Sequences where values can be updated. | verify |
| IO_ITERATOR | Iterators to read and write from/to a container in linear order. | verify |
| MUTABLE_SEQUENCE_ITERATOR | Iterators to read from and update mutable sequences. | verify |
| ARRAY | Indexable containers with arbitrary bounds, whose elements are stored in a continuous memory area. | verify |
| INDEX_ITERATOR | Iterators over sequences that access elements directly through an integer index. | verify |
| ARRAY_ITERATOR | Iterators over mutable sequences that allow only traversal, search and replacement. | verify |
| ARRAYED_LIST | Lists implemented as ring buffers. | verify |
| ARRAYED_LIST_ITERATOR | Iterators over arrayed lists. | verify |
| ARRAY2 | Two-dimensional arrays. | verify |
| LIST | Indexable containers, where elements can be inserted and removed at any position. | verify |
| LIST_ITERATOR | Iterators over lists. | verify |
| CELL | Cells containing an item. | verify |
| LINKABLE | Cells that can be linked to another cell. | verify |
| LINKED_LIST | Singly linked lists. | verify |
| LINKED_LIST_ITERATOR | Iterators over linked lists. | verify |
| DOUBLY_LINKABLE | Cells that can be linked to two neighbour cells. | verify |
| DOUBLY_LINKED_LIST | Doubly linked lists. | verify |
| DOUBLY_LINKED_LIST_ITERATOR | Iterators over doubly-linked lists. | verify |
| DISPENSER | Containers that can be extended with values and make only one element accessible at a time. | verify |
| STACK | Dispensers where the latest added element is accessible. | verify |
| LINKED_STACK | Linked implementation of stacks. | verify |
| LINKED_STACK_ITERATOR | Iterators over linked stacks. | verify |
| QUEUE | Dispensers where the earliest added element is accessible. | verify |
| LINKED_QUEUE | Linked implementation of queues. | verify |
| LINKED_QUEUE_ITERATOR | Iterators over linked queues. | verify |
| LOCK | Helper ghost objects that prevent container items from unwanted modifications. | verify |
| LOCKER | Containers that use a lock to protect their items. | verify |
| MAP | Containers where values are associated with keys. | verify |
| MAP_ITERATOR | Iterators to read from maps in linear order. | verify |
| TABLE | Maps where key-value pairs can be updated, added and removed. | verify |
| TABLE_ITERATOR | Iterators to read from and update tables. | verify |
| HASHABLE | Hahsable object. | verify |
| HASH_LOCK | Helper ghost objects that prevent hashable container items from unwanted modifications. | verify |
| HASH_TABLE | Hash tables with hash function provided by HASHABLE and object equality. | verify |
| HASH_TABLE_ITERATOR | Iterators over hash tables. | verify |
| SET | Container where all elements are unique with respect to object equality. | verify |
| SET_ITERATOR | Iterators over sets, allowing efficient search. | verify |
| HASH_SET | Hash sets with hash function provided by HASHABLE and object equality. | verify |
| HASH_SET_ITERATOR | Iterators over hash sets. | verify |
| RANDOM | Streams that provide pseudorandom integer values | verify |